\begin{tabbing}
bframe{-}p(${\it es}$;$i$;$k$;$L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$alle{-}at(${\it es}$;$i$;$e$.\=es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd\+
\\[0ex]$\Rightarrow$ (\=$\forall$$l$:IdLnk.\+
\\[0ex]$\neg$($l$ $\in$ $L$ $\in$ IdLnk) $\Rightarrow$ es{-}sends(${\it es}$; $l$; $e$) $=$ nil $\in$ es{-}Msg(${\it es}$) List))
\-\-
\end{tabbing}